In type theory, a type system has the property of subject reduction if evaluation of expressions does not cause their type to change. Formally, if expression e1 →* e2 and Γ ⊢ e1 : τ then Γ ⊢ e2 : τ.
Together with progress, it is an important meta-theoretical property for establishing type soundness of a type system. Its proof usually relies on a substitution lemma.